$\forall$${\it es}$:ES, $e$:E, $P$:(\{$a$:E$\mid$ loc($a$) = loc($e$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$a$:\{$a$:E$\mid$ loc($a$) = loc($e$) $\in$ Id\} . Dec($P$($a$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it e'}$$\leq$$e$.$P$(${\it e'}$) $\Leftarrow\!\Rightarrow$ $P$($e$) $\vee$ $\exists$${\it e'}$$\leq$$e$.($\neg$($P$(${\it e'}$) $\Leftarrow\!\Rightarrow$ $P$($e$))) \& $\forall$${\it e''}$$\in$(${\it e'}$,$e$].$P$(${\it e''}$) $\Leftarrow\!\Rightarrow$ $P$($e$))